// Copyright 2007-2009, Stanford University. All Rights Reserved.
// Copyright 2010-2011, Dependable Systems Lab, EPFL. All Rights Reserved.
// Copyright 2012, Google Inc. All Rights Reserved.
//
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are
// met:
//
//     * Redistributions of source code must retain the above copyright
// notice, this list of conditions and the following disclaimers.
//     * Redistributions in binary form must reproduce the above
// copyright notice, this list of conditions and the following disclaimers
// in the documentation and/or other materials provided with the
// distribution.
//     * Neither the names of the klee Team, Stanford University, nor the
// names of its contributors may be used to endorse or promote
// products derived from the software without specific prior
// written permission. Neither the names of the Dependable Systems
// Laboratory, EPFL, nor the names of its contributors may be used to
// endorse or promote products derived from the software without prior
// written permission. Neither the names of Google Inc. nor the names of
// its contributors may be used to endorse or promote products derived from
// the software without specific prior written permission.
//
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
// OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

#ifndef SRC_EXPR_EXPRVISITOR_H_
#define SRC_EXPR_EXPRVISITOR_H_

#include "ExprHashMap.h"

namespace seven_summits {
namespace util {

template<class T> class ref;

}  // namespace util
}  // namespace seven_summits


namespace seven_summits {
namespace expr {

using seven_summits::util::ref;

class ExprVisitor {
protected:
  // typed variant, but non-virtual for efficiency
  class Action {
  public:
    enum Kind { SkipChildren, DoChildren, ChangeTo };

  private:
    //      Action() {}
    Action(Kind _kind)
      : kind(_kind), argument(ConstantExpr::alloc(0, Expr::Bool)) {}
    Action(Kind _kind, const ref<Expr> &_argument)
      : kind(_kind), argument(_argument) {}

    friend class ExprVisitor;

  public:
    Kind kind;
    ref<Expr> argument;

    static Action changeTo(const ref<Expr> &expr) {
      return Action(ChangeTo,expr);
    }
    static Action doChildren() { return Action(DoChildren); }
    static Action skipChildren() { return Action(SkipChildren); }
  };

protected:
  explicit
  ExprVisitor(bool _recursive=false) : recursive(_recursive) {}
  virtual ~ExprVisitor() {}

  virtual Action visitExpr(const Expr&);
  virtual Action visitExprPost(const Expr&);

  virtual Action visitNotOptimized(const NotOptimizedExpr&);
  virtual Action visitRead(const ReadExpr&);
  virtual Action visitSelect(const SelectExpr&);
  virtual Action visitConcat(const ConcatExpr&);
  virtual Action visitExtract(const ExtractExpr&);
  virtual Action visitZExt(const ZExtExpr&);
  virtual Action visitSExt(const SExtExpr&);
  virtual Action visitAdd(const AddExpr&);
  virtual Action visitSub(const SubExpr&);
  virtual Action visitMul(const MulExpr&);
  virtual Action visitUDiv(const UDivExpr&);
  virtual Action visitSDiv(const SDivExpr&);
  virtual Action visitURem(const URemExpr&);
  virtual Action visitSRem(const SRemExpr&);
  virtual Action visitNot(const NotExpr&);
  virtual Action visitAnd(const AndExpr&);
  virtual Action visitOr(const OrExpr&);
  virtual Action visitXor(const XorExpr&);
  virtual Action visitShl(const ShlExpr&);
  virtual Action visitLShr(const LShrExpr&);
  virtual Action visitAShr(const AShrExpr&);
  virtual Action visitEq(const EqExpr&);
  virtual Action visitNe(const NeExpr&);
  virtual Action visitUlt(const UltExpr&);
  virtual Action visitUle(const UleExpr&);
  virtual Action visitUgt(const UgtExpr&);
  virtual Action visitUge(const UgeExpr&);
  virtual Action visitSlt(const SltExpr&);
  virtual Action visitSle(const SleExpr&);
  virtual Action visitSgt(const SgtExpr&);
  virtual Action visitSge(const SgeExpr&);

private:
  typedef ExprHashMap< ref<Expr> > visited_ty;
  visited_ty visited;
  bool recursive;

  ref<Expr> visitActual(const ref<Expr> &e);

public:
  // apply the visitor to the expression and return a possibly
  // modified new expression.
  ref<Expr> visit(const ref<Expr> &e);
};

}  // namespace expr
}  // namespace seven_summits

#endif  // SRC_EXPR_EXPRVISITOR_H_
